Cubical Type Theory
https://ncatlab.org/nlab/show/cubical+type+theory
https://arxiv.org/abs/1611.02108
https://1lab.dev/index.html
https://www.youtube.com/playlist?list=PL0OBHndHAAZrGQEkOZGyJu7S7KudAJ8M9
https://twitter.com/masahiro_sakai/status/1172911079732547584
https://doisinkidney.com/posts/2019-04-17-cubical-probability.html
Cubical Type Theory は HoTT の univalence axiom をちゃんと計算できる形に解釈できる理論で、直観的にはパスをI=[0,1]からの関数として解釈する。実装としてはもともとcubicalttという実験的なプロトタイプ実装はあったけど、今回Agdaを拡張してfull-fledgedな実装を提案したという感じ。 ref
ぜんぜんわからんmrsekut.icon
ホモトピー型理論を知らないと全く理解出来なさそうmrsekut.icon
まず、 Homotopy Type Theory は、 Functional Extensionality と Univalence Axiom と Higher Inductive Types の存在が成り立つ型理論と、その上で展開される数学のことを、総称として呼んだものだと、私は捉えています。ref
どうやって、これらの命題を成り立たせるか。 Homotopy Type Theory が産まれた当時は、これらを公理として追加する方法しかありませんでした。しかし、これでは計算が公理の所で止まってしまいます。
そこで登場したのが Cubical Type Theory で、これは計算が途中で止まらないにも関わらず Functional Extensionality と Univalence Axiom が成り立ちます。
私の理解では、こうです。